(set-logic QF_LIA)
(declare-const x3 Int)
(declare-const x Int)
(declare-fun |:| () Int)
(declare-fun |s:| () Int)
(declare-fun s () Int)
(declare-fun |::| () Int)
(declare-fun t () Int)
(assert (and (or (= 0 s) (and (= |::| 1) (= -2 (* -1 |:|)))) (or (and (= -1 |s:|) (= 0 x3) (= 0 x) (> 0 (+ s (* -1 t)))) (and (= 0 s) (> 0 (+ s (* -1 t))) (= 0 (+ |:| (* -50 t))) (or (= 0 s) (and (= |::| 1) (= -2 (* -1 |:|))))))))
(check-sat)
(check-sat)
